1"""Stage 5: how tight is the boundary lower bound? Computes the exact2beta_18(n) for 26 <= n <= 40 by solving F(n,18,b) upward from b = 12 with3the project encoder (CaDiCaL); the certificate margin is beta_18(n) - 12.4Models are re-checked by direct counting. Output: results/robustness/margin.json"""5import json, os, sys, time6ROOT = os.path.dirname(os.path.dirname(os.path.dirname(os.path.abspath(__file__)))); os.chdir(ROOT)7sys.path.insert(0, os.path.join(ROOT, ".pydeps")); sys.path.insert(0, os.path.join(ROOT, "code"))8from pysat.solvers import Solver9from sat_or_ilp_solver import boundary_clauses10def nbrs(n, k=5):11 A = {}12 for i in range(n):13 A[i] = {(i + 1) % n, (i - 1) % n, n + i}; A[n + i] = {n + (i + k) % n, n + (i - k) % n, i}14 return A15out = []16for n in range(26, 41):17 A = nbrs(n); t0 = time.time(); rec = {"n": n}18 for b in range(12, 20):19 cl, x, z, nv = boundary_clauses(n, 5, 18, b)20 with Solver(name="cadical195", bootstrap_with=cl) as sv:21 sat = sv.solve(); model = sv.get_model() if sat else None22 if sat:23 X = [w for w in range(2 * n) if model[x[w] - 1] > 0]; Xs = set(X)24 bd = len({w for q in X for w in A[q] if w not in Xs})25 rec.update({"beta_18": b, "model_boundary_recount": bd, "model_size": len(X), "margin": b - 12,26 "X": ["%s%d" % ("u" if w < n else "v", w % n) for w in X]})27 break28 rec["seconds"] = round(time.time() - t0, 1); out.append(rec); print(rec, flush=True)29json.dump(out, open("results/robustness/margin.json", "w"), indent=1)30