#!/usr/bin/env python3
"""
Cross-check: decide (k+1)-colourability of J(2k,k) with NO symmetry break at all
(full search, independent vertex ordering), to remove any reliance on the
symmetry argument used in settle_835.py. Uses DSATUR-style MRV backtracking.
"""
import sys, itertools, json, time
def build(n,k):
    V=list(itertools.combinations(range(n),k)); S=[frozenset(s) for s in V]
    adj=[set() for _ in V]
    for i in range(len(V)):
        for j in range(i+1,len(V)):
            if len(S[i]&S[j])==k-1: adj[i].add(j); adj[j].add(i)
    return V,adj
def colourable(nV,adj,ncol):
    colour=[-1]*nV; nodes=[0]
    import sys as _s; _s.setrecursionlimit(10000)
    def sat_deg(v): return len({colour[w] for w in adj[v] if colour[w]>=0})
    def rec():
        nodes[0]+=1
        # DSATUR: pick uncoloured vertex maximizing saturation, tie-break by degree
        best=-1;bk=(-1,-1)
        for v in range(nV):
            if colour[v]==-1:
                key=(sat_deg(v),len(adj[v]))
                if key>bk: bk=key;best=v
        if best==-1: return True
        v=best; used={colour[w] for w in adj[v] if colour[w]>=0}
        for c in range(ncol):
            if c not in used:
                colour[v]=c
                if rec(): return True
                colour[v]=-1
        return False
    ok=rec(); return ok,nodes[0]
if __name__=="__main__":
    for k in [int(x) for x in sys.argv[1:]] or [2,3,4]:
        n=2*k;ncol=k+1;V,adj=build(n,k);nV=len(V)
        t0=time.time();ok,nd=colourable(nV,adj,ncol);dt=round(time.time()-t0,3)
        print(json.dumps({"k":k,"n":n,"colours":ncol,"vertices":nV,
            "colourable_no_symmetry_break":ok,"nodes":nd,"seconds":dt,
            "conclusion":("835(%d) YES"%k) if ok else ("835(%d) NO"%k)}))