1"""Driver for the exhaustive C oracle (brute_force.c): for a given n, k, finds2Z(P(n,k)) by increasing cardinality s, in parallel over the lowest vertex id3m0 (2n independent jobs per s), with orbit reduction under D_n (P3).45Also contains a pure-Python reference enumeration (no symmetry reduction) used6to cross-validate the C program on tiny cases (P(5,2) and P(11,5) at s <= 5).78Output: results/brute_force_runs.jsonl (one record per (n,k,s)) and the9value table results/brute_force_values.json.10"""11import itertools12import json13import os14import subprocess15import sys16import time17from concurrent.futures import ThreadPoolExecutor1819import common20from closure_oracle import closure_fast21from graph_constructor import adjacency_masks, edge_list_sha256, edges_formula2223BIN = os.path.join(common.ROOT, "code", "brute_force")242526def build_binary():27 src = os.path.join(common.ROOT, "code", "brute_force.c")28 if not os.path.exists(BIN) or os.path.getmtime(BIN) < os.path.getmtime(src):29 subprocess.run(["gcc", "-O2", "-o", BIN, src], check=True)303132def run_one(n, k, s, m0):33 out = subprocess.run([BIN, str(n), str(k), str(s), str(m0)], capture_output=True, text=True, check=True).stdout34 d = {}35 for tok in out.split():36 key, _, val = tok.partition("=")37 d[key] = val38 return d394041def count_size(n, k, s, workers=16):42 """Enumerates all s-subsets (split over m0). Returns (enumerated, tested, forcing, witness or None, wall)."""43 t0 = time.time()44 with ThreadPoolExecutor(max_workers=workers) as ex:45 parts = list(ex.map(lambda m0: run_one(n, k, s, m0), range(2 * n)))46 enumerated = sum(int(p["enumerated"]) for p in parts)47 tested = sum(int(p["tested"]) for p in parts)48 forcing = sum(int(p["forcing"]) for p in parts)49 witness = next((p["witness"] for p in parts if "witness" in p), None)50 return enumerated, tested, forcing, witness, time.time() - t0515253def python_reference(n, k, s):54 """No symmetry reduction: counts all forcing s-subsets (for tiny cases only)."""55 adj = adjacency_masks(n, k)56 N = 2 * n57 full = (1 << N) - 158 cnt = 059 for comb in itertools.combinations(range(N), s):60 m = 061 for w in comb:62 m |= 1 << w63 if closure_fast(adj, m) == full:64 cnt += 165 return cnt666768def find_Z(n, k, s_start=1, s_max=12, time_limit=1800, workers=16):69 """Returns (Z or None, records). Each size s < Z is exhausted (forcing == 0)."""70 records = []71 t_total = time.time()72 for s in range(s_start, s_max + 1):73 if time.time() - t_total > time_limit:74 return None, records75 if s >= 12 and n >= 12:76 # Z <= 12 by the explicit construction P7 (replayed in verify_upper_bounds.py);77 # all sizes <= 11 have been exhausted above, so Z = 12 without enumerating 12-sets.78 rec = {"n": n, "k": k, "s": s, "enumerated_subsets": 0, "orbit_representatives_tested": 0,79 "forcing_representatives": 1, "witness": ",".join("u%d" % i for i in range(12)),80 "witness_source": "P7 construction (not enumerated)", "wall_seconds": 0.0,81 "utc": common.utcnow(), "graph_sha256": edge_list_sha256(edges_formula(n, k))}82 records.append(rec)83 common.append_jsonl(os.path.join(common.RESULTS, "brute_force_runs.jsonl"), rec)84 return s, records85 enumerated, tested, forcing, witness, wall = count_size(n, k, s, workers)86 rec = {"n": n, "k": k, "s": s, "enumerated_subsets": enumerated, "orbit_representatives_tested": tested,87 "forcing_representatives": forcing, "witness": witness, "wall_seconds": round(wall, 3),88 "utc": common.utcnow(), "graph_sha256": edge_list_sha256(edges_formula(n, k))}89 records.append(rec)90 common.append_jsonl(os.path.join(common.RESULTS, "brute_force_runs.jsonl"), rec)91 print(json.dumps(rec), flush=True)92 if forcing:93 return s, records94 return None, records959697if __name__ == "__main__":98 build_binary()99 # cross-validation of the C oracle against the Python reference on tiny cases100 checks = []101 for (n, k, s) in [(5, 2, 4), (5, 2, 5), (11, 5, 5)]:102 ref = python_reference(n, k, s)103 enumerated, tested, forcing, witness, wall = count_size(n, k, s)104 # orbit reduction: forcing representatives > 0 iff reference count > 0105 checks.append({"n": n, "k": k, "s": s, "python_forcing_subsets": ref, "c_forcing_representatives": forcing,106 "agree": (ref > 0) == (forcing > 0)})107 print(checks[-1])108 assert all(c["agree"] for c in checks)109 with open(os.path.join(common.RESULTS, "brute_force_crosscheck.json"), "w") as f:110 json.dump(checks, f, indent=1)111 ns = [int(a) for a in sys.argv[1:]] or [11, 12, 13, 14]112 k = 5113 values = {}114 if os.path.exists(os.path.join(common.RESULTS, "brute_force_values.json")):115 values = json.load(open(os.path.join(common.RESULTS, "brute_force_values.json")))116 for n in ns:117 Z, recs = find_Z(n, k, s_start=max(1, (4 if n >= 11 else 1)), time_limit=float(os.environ.get("BF_TIME_LIMIT", "1800")))118 values[str(n)] = {"Z": Z, "sizes_exhausted": [r["s"] for r in recs if r["forcing_representatives"] == 0],119 "witness": recs[-1]["witness"] if recs and recs[-1]["forcing_representatives"] else None,120 "total_wall_seconds": round(sum(r["wall_seconds"] for r in recs), 3)}121 print("n=%d Z=%s" % (n, Z), flush=True)122 with open(os.path.join(common.RESULTS, "brute_force_values.json"), "w") as f:123 json.dump(values, f, indent=1)124