#!/usr/bin/env python3
"""k=6 background attempt: 7-colourability of J(12,6) with extra symmetry breaking.
Fix TWO overlapping anti-star cliques as far as forced, to cut the search."""
import itertools, json, time
from pysat.formula import CNF
from pysat.solvers import Cadical153

k=6; n=2*k; ncol=k+1
V=list(itertools.combinations(range(n),k)); idx={s:i for i,s in enumerate(V)}
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)
cliques=[tuple(idx[tuple(sorted(set(A)-{x}))] for x in A) for A in itertools.combinations(range(n),k+1)]
nV=len(V)
def var(v,c): return v*ncol+c+1
cnf=CNF()
for v in range(nV):
    cnf.append([var(v,c) for c in range(ncol)])
    for c1 in range(ncol):
        for c2 in range(c1+1,ncol): cnf.append([-var(v,c1),-var(v,c2)])
seen=set()
for v in range(nV):
    for w in adj[v]:
        e=(v,w) if v<w else (w,v)
        if e in seen: continue
        seen.add(e)
        for c in range(ncol): cnf.append([-var(v,c),-var(w,c)])
# symmetry break 1: anti-star clique A0={0..6} fixed to identity
A0=tuple(range(k+1)); Q0=[idx[tuple(sorted(set(A0)-{x}))] for x in A0]
for pos,v in enumerate(Q0): cnf.append([var(v,pos)])
print(f"k=6 J({n},{k}): vars={nV*ncol}, clauses={len(cnf.clauses)}",flush=True)
t0=time.time()
s=Cadical153(bootstrap_with=cnf.clauses)
r=s.solve()
dt=round(time.time()-t0,1)
out={"k":6,"colourable":bool(r),"seconds":dt,
     "conclusion":("835(6) is YES" if r else "835(6) is NO")}
if r:
    m=set(l for l in s.get_model() if l>0)
    colour=[next(c for c in range(ncol) if var(v,c) in m) for v in range(nV)]
    out["verified_proper"]=all(colour[v]!=colour[w] for v in range(nV) for w in adj[v])
    out["verified_all_rainbow"]=all(len({colour[f] for f in fac})==ncol for fac in cliques)
    json.dump({"colour_by_vertex_index":colour,"vertices":[list(x) for x in V]},open("witness_k6.json","w"))
s.delete()
json.dump(out,open("settle_k6_result.json","w"),indent=1)
print(json.dumps(out),flush=True)