1"""Stage 5: cross-check of the boundary formula F(n,p,b) (Lemma 3.4, project2encoder code/sat_or_ilp_solver.py:boundary_clauses) against the exhaustive3boundary distribution computed by code/robustness/beta_brute.c (no SAT, no4symmetry reduction).56For every (n,p) in the beta_brute output:7 * beta_brute's minimum must equal the SAT-derived table value in8 results/tables/boundary_table.csv wherever the table has an exact entry9 (entries '12' in the table mean '>= 12' and are compared accordingly);10 * F(n,p,b) must be UNSAT for b = beta - 1 and SAT for b = beta (both the11 'exactly p' and the 'at most b' sides of the encoding are exercised on12 UNSAT instances, which is the direction the proof relies on);13 * the model returned at b = beta must be a p-set of boundary <= beta by14 direct counting here.15Output: results/robustness/boundary_encoding_check.json16"""17import csv18import json19import os20import re21import sys2223ROOT = os.path.dirname(os.path.dirname(os.path.dirname(os.path.abspath(__file__))))24os.chdir(ROOT)25sys.path.insert(0, os.path.join(ROOT, ".pydeps"))26sys.path.insert(0, os.path.join(ROOT, "code"))2728from pysat.solvers import Solver # noqa: E40229from sat_or_ilp_solver import boundary_clauses # noqa: E402303132def nbrs(n, k=5):33 A = {}34 for i in range(n):35 A[i] = {(i + 1) % n, (i - 1) % n, n + i}36 A[n + i] = {n + (i + k) % n, n + (i - k) % n, i}37 return A383940def solve(n, p, b):41 cl, x, z, nv = boundary_clauses(n, 5, p, b)42 with Solver(name="cadical195", bootstrap_with=cl) as sv:43 sat = sv.solve()44 model = sv.get_model() if sat else None45 X = None46 if sat:47 X = [w for w in range(2 * n) if model[x[w] - 1] > 0]48 return sat, X495051def main():52 table = {}53 rows = list(csv.DictReader(open("results/tables/boundary_table.csv")))54 for r in rows:55 p = int(r["p"])56 for col, val in r.items():57 if col != "p" and val not in ("", None):58 table[(int(col), p)] = 12 if val.strip().startswith(">=") else int(val)59 brute = {}60 for line in open("results/robustness/beta_brute_stdout.txt"):61 m = re.match(r"n=(\d+) k=5 p=(\d+) subsets=(\d+) beta=(-?\d+) hist=(.*)", line)62 if m:63 n, p, subs, beta = int(m.group(1)), int(m.group(2)), int(m.group(3)), int(m.group(4))64 hist = dict(int(a) for a in ()) if False else {int(h.split(":")[0]): int(h.split(":")[1]) for h in m.group(5).split()}65 brute[(n, p)] = (beta, subs, hist)66 out = {"instances": [], "table_comparisons": []}67 A_cache = {}68 for (n, p), (beta, subs, hist) in sorted(brute.items()):69 A = A_cache.setdefault(n, nbrs(n))70 rec = {"n": n, "p": p, "beta_brute": beta, "subsets": subs}71 if (n, p) in table:72 tv = table[(n, p)]73 rec["table_value"] = tv74 rec["table_consistent"] = (tv == beta) if tv <= 11 else (beta >= 12)75 out["table_comparisons"].append(rec["table_consistent"])76 # SAT at beta, UNSAT at beta-177 s_lo, _ = solve(n, p, beta - 1) if beta >= 1 else (False, None)78 s_hi, X = solve(n, p, beta)79 rec["unsat_at_beta_minus_1"] = (s_lo is False)80 rec["sat_at_beta"] = bool(s_hi)81 if s_hi:82 Xs = set(X)83 bd = {w for x in X for w in A[x] if w not in Xs}84 rec["model_size_ok"] = len(X) == p85 rec["model_boundary"] = len(bd)86 rec["model_boundary_ok"] = len(bd) <= beta87 rec["ok"] = rec["unsat_at_beta_minus_1"] and rec["sat_at_beta"] and rec.get("model_size_ok", False) and rec.get("model_boundary_ok", False) and rec.get("table_consistent", True)88 out["instances"].append(rec)89 out["num_instances"] = len(out["instances"])90 out["all_ok"] = all(r["ok"] for r in out["instances"])91 out["table_cells_compared"] = len(out["table_comparisons"])92 out["table_cells_consistent"] = sum(out["table_comparisons"])93 json.dump(out, open("results/robustness/boundary_encoding_check.json", "w"), indent=1)94 print("instances:", out["num_instances"], "all ok:", out["all_ok"], "table cells compared:", out["table_cells_compared"], "consistent:", out["table_cells_consistent"])95 for r in out["instances"]:96 if not r["ok"]:97 print("FAIL", r)9899100if __name__ == "__main__":101 main()102