1"""Stage 5: stress tests for the column-deletion lemma P9 and the reduction2pipeline of Lemma 3.2 (results/derivations.md), written from scratch.34Test D1 (exhaustive, small X). For 13 <= n <= 30 and every X with |X| <= 25(|X| = 3 for n <= 20) supported on columns 11..n-1 (both layers), check the6strong form of P9: f(N[X]) = N[X'] and f(dX) = dX' as SETS (hence equal7sizes), where f deletes column 5 and shifts columns > 5 down by one.89Test D2 (negative control). Same, but X is allowed to meet column 10 (gap10of only 10 empty columns). Here the hypothesis of P9 fails and we count the11cases where f is undefined on dX (a neighbour of X sits in the deleted12column) or f(dX) != dX'. A nonzero count shows the test has teeth.1314Test D3 (pipeline on near-extremal sets). For p in {16, 18} and several n0,15obtain an X with |dX| <= 11 from the project's own SAT formula with columns160..9 forced empty (project encoder, model re-checked here by direct17counting), then (a) INSERT a column at position 5 repeatedly up to n0 + 2518and (b) DELETE it back down to n0; after every step the boundary is19recomputed from scratch in the new graph and must be unchanged, and the20final set must equal the original.21Output: results/robustness/deletion_lemma.json22"""23import itertools24import json25import os26import sys2728ROOT = os.path.dirname(os.path.dirname(os.path.dirname(os.path.abspath(__file__))))29os.chdir(ROOT)30sys.path.insert(0, os.path.join(ROOT, ".pydeps"))31sys.path.insert(0, os.path.join(ROOT, "code"))323334def adj(n, k=5):35 A = {}36 for i in range(n):37 A[("u", i)] = {("u", (i + 1) % n), ("u", (i - 1) % n), ("v", i)}38 A[("v", i)] = {("v", (i + k) % n), ("v", (i - k) % n), ("u", i)}39 return A404142def closed_nbhd(A, X):43 return set(X) | {w for x in X for w in A[x]}444546def boundary(A, X):47 return closed_nbhd(A, X) - set(X)484950def f_del(w):51 layer, i = w52 if i == 5:53 return None54 return (layer, i if i < 5 else i - 1)555657def f_ins(w):58 layer, i = w59 return (layer, i if i < 5 else i + 1)606162def check_strong(n, X):63 A, A1 = adj(n), adj(n - 1)64 NX = closed_nbhd(A, X)65 if any(f_del(w) is None for w in NX):66 return False, "deleted vertex in N[X]"67 X1 = {f_del(w) for w in X}68 ok = {f_del(w) for w in NX} == closed_nbhd(A1, X1) and {f_del(w) for w in boundary(A, X)} == boundary(A1, X1)69 return ok, ""707172def main():73 out = {}74 # D175 d1_cases = d1_fail = 076 for n in range(13, 31):77 verts = [(l, i) for i in range(11, n) for l in ("u", "v")]78 sizes = [1, 2] + ([3] if n <= 20 else [])79 for s in sizes:80 for X in itertools.combinations(verts, s):81 d1_cases += 182 ok, _ = check_strong(n, set(X))83 if not ok:84 d1_fail += 185 out["D1"] = {"cases": d1_cases, "failures": d1_fail, "n_range": [13, 30], "sizes": "1,2 (and 3 for n<=20)"}86 # D2 negative control87 d2_cases = d2_undefined = d2_mismatch = d2_size_change = 088 examples = []89 for n in range(13, 31):90 col10 = [("u", 10), ("v", 10)]91 others = [(l, i) for i in range(10, n) for l in ("u", "v")]92 for s in (1, 2):93 for X in itertools.combinations(others, s):94 if not any(w in col10 for w in X):95 continue96 d2_cases += 197 A, A1 = adj(n), adj(n - 1)98 NX = closed_nbhd(A, X)99 X1 = {f_del(w) for w in X}100 b1 = boundary(A1, X1)101 if any(f_del(w) is None for w in NX):102 d2_undefined += 1103 if len(b1) != len(boundary(A, X)):104 d2_size_change += 1105 if len(examples) < 3:106 examples.append({"n": n, "X": sorted(X), "boundary_before": len(boundary(A, X)), "boundary_after": len(b1)})107 elif {f_del(w) for w in boundary(A, X)} != b1:108 d2_mismatch += 1109 out["D2"] = {"cases": d2_cases, "f_undefined_on_N[X]": d2_undefined, "set_mismatch": d2_mismatch,110 "boundary_size_changed": d2_size_change, "examples": examples}111 # D3 pipeline112 from sat_or_ilp_solver import boundary_clauses # project encoder (only to obtain test instances)113 from pysat.solvers import Solver114 d3 = []115 for (p, n0) in [(16, 22), (16, 26), (16, 30), (18, 22), (18, 23), (18, 25), (20, 24)]:116 cl, x, z, nv = boundary_clauses(n0, 5, p, 11)117 # force columns 0..9 empty (rotation normalisation replaced by an explicit gap)118 cl = [c for c in cl if c != [x[0], x[n0]]] # drop the project's x_{u0} v x_{v0} clause119 for i in range(10):120 cl.append([-x[i]])121 cl.append([-x[n0 + i]])122 with Solver(name="cadical195", bootstrap_with=cl) as sv:123 sat = sv.solve()124 model = sv.get_model() if sat else None125 rec = {"p": p, "n0": n0, "instance_found": bool(sat)}126 if sat:127 X = {("u" if w < n0 else "v", w if w < n0 else w - n0) for w in range(2 * n0) if model[x[w] - 1] > 0}128 A = adj(n0)129 b0 = len(boundary(A, X))130 rec["boundary_n0"] = b0131 rec["size_ok"] = len(X) == p132 rec["gap_ok"] = all(w[1] >= 10 for w in X)133 # insert up to n0+25134 cur, n = set(X), n0135 trail = []136 okall = True137 for step in range(25):138 cur = {f_ins(w) for w in cur}139 n += 1140 b = len(boundary(adj(n), cur))141 trail.append(b)142 okall &= (b == b0)143 rec["insert_boundaries_n0+1..n0+25_all_equal"] = okall144 okdel = True145 for step in range(25):146 cur = {f_del(w) for w in cur}147 n -= 1148 b = len(boundary(adj(n), cur))149 okdel &= (b == b0)150 rec["delete_back_all_equal"] = okdel151 rec["returned_to_original_set"] = (cur == X and n == n0)152 rec["ok"] = rec["size_ok"] and rec["gap_ok"] and okall and okdel and rec["returned_to_original_set"] and b0 <= 11153 d3.append(rec)154 out["D3"] = d3155 out["D1_ok"] = d1_fail == 0156 out["D3_ok"] = all(r["ok"] for r in d3 if r["instance_found"])157 out["D3_instances_found"] = sum(1 for r in d3 if r["instance_found"])158 json.dump(out, open("results/robustness/deletion_lemma.json", "w"), indent=1)159 print(json.dumps({k: out[k] for k in ("D1", "D2", "D1_ok", "D3_ok", "D3_instances_found")}, indent=None))160 for r in d3:161 print(r)162163164if __name__ == "__main__":165 main()166